$\forall$$A$:MsgA, $i$:Id.
\\[0ex]AtomFree(ds($A$))
\\[0ex]$\Rightarrow$ AtomFree(da($A$))
\\[0ex]$\Rightarrow$ AtomFree(Type;\{$m$:($l$:IdLnk$\times$$t$:Id$\times$$A$.dout($l$,$t$))$\mid$ source(mlnk($m$)) $=$ $i$ \})